Here comes the second issue of my blog post! I have started my university semester, and it is going to be week 2 soon. I found that time management is far more easier if you work / study at home, without those commutes and travelling. Working / Studying online makes the time management turned into stamina management. You just got to find a method or a schedule to let yourself focus on something.
Spaced repitition
Spaced repetition is one of the method I am attempting to practice. It is a technique for efficient memorization instead of attemping to memorize by 'cramming', memorization can be done far more efficient by instead spacing out each review, with increasing durations as one learns the item, with the scheduling done by software.
This is well suited for people who are balencing a job while studying for a degree. As you work on workday, you can revise previous courses at day night, and move on to new topic at weekends. This is however, need to have strong self-control and good system to review your learning. So I am trying to construct a system / schedule for my daily routine, and see if it works.
A Programming Language I am making
I have been developing a programming language for myself while learning compiler engineering. And now I found myself falling into the pit of type theory quickly.
The language I am developing is called Topos, it comes from the Greek that refers to a method for developing arguments, and now we refer it to the category that behaves like the presheaf sets on topological spaces. Personally, I prefer the first definition as it is more understanable, and a programming langues does help us to construct arguments in some certain extend.
The initial idea was making a programming language to empower user to learn how computers work, in a designed abstraction. By adding more code incrementally and giving more hints to the compiler, for example, type annotation and type level programming, could increase the verified portion of program. Potentially it will do type erasure and allow performant code generated.
In topos I wished to make writing proofs easily, by building patterns and constructs on rigid theory.
I hope this can also empower more and more programmers to keep an eye on the program safety, and even more, the mathematical foundations.
To accomplish this, the programming language we make shall allow newcomers to learn mathematical thinking gradually and reduce the costs of writing safe programs in real world.
The topos compiler and the language design would be exist without the prior work of others. During the development of topos compiler I had read many other projects and here I list down the notable feature of others.
Haskell
-
Non-strict evaluation, it only computes when neccessary, and lots of compiler optimizations focusing on making it fast. Which is ...
-
STG, spineless tagless graph reduction machine. It allows potentially out-of-order optimization being made, and implement non-strict semantics, which makes the Haskell language 'lazy'.
-
Rewrite rules, because of the lazy evaluation and the precense of STG IR, it allows programmer to specific a set of rules that will do aggressive expression rewrite during runtime.
As far as I know, Scaba Hruska is working on whole program optimization and strict functional languages backend, GRIN compiler.
Sixty / Sixten
- Command based programming / Query based compiler architectures. It used a dependent hashmap to store commands and dispatch on-demand. By implementing this in a compiler, recompiling a project after having made a few changes we only recompile what is affected by the changes
Idris / Idris 2
-
Linear types, it used the Quantitative Type Theory.
-
Optional totality check, it provide an escape hatch for developers, making dependent typed programming practical.
-
Multiple backend, idris recently got ported into Racket which runs on Chez Scheme.
Setoidtt (previously setoidtt-proto)
- Dependent types
Cyclone
-
Region-based memory management, it replaces the use of garbage-collected memory with faster, scope-nested memory regions (arenas).
-
Linear/affine types, an experimental application of the linear logic (substructal logic). So we can get safe, deterministic memory management without run-time GC bookkeeping costs.
Which also leads to the Rust's lifetime, another explicit region annotations for low level memory management strategies.
Rust
-
unsafe annotation, and a comprehensive handbook disccussing the black magic of compiler. Allowing programmers to write safe, performant logic which the compiler cannot verify as safe.
-
Traits, polymorphic dispatch.
Reference
- Spaced repetition memory technique
- The Facinating Influence of Cyclone
- The Achitecture of Open Source Applications - The GHC - although the GHC had changed so much since that, it is still fun to read, to know how complex GHC is.
- Lazy evaluation illustrated for Haskell divers
- Query-based compiler architectures